Inference at * 1 1 
Iof proof for Lemma nat ind tp:



1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. i : 
  P(i) 

latex

 by (%S% \p.AbSetHD (get_int_arg `hn` p) p) 

latex

 1: 

 1: 4. i : 
 1: 5. i  0 
 1:   P(i)
 .

Definitions	t  T, x:A. B(x),
Lemmas	nat properties